package de.rs.espresso.algorithms.tautology;

import java.util.ArrayList;
import java.util.List;

import de.rs.espresso.covers.DefaultCover;
import de.rs.espresso.cubes.CubeFactory;
import de.rs.espresso.cubes.FreezedCube;
import de.rs.espresso.interfaces.ICover;
import de.rs.espresso.interfaces.ICube;
import de.rs.espresso.interfaces.IGlobalInformation;
import de.rs.espresso.tools.Statistics;

/**
 * Uses the same Algorithm as {@link SimpleTautologyCheck}.<br>
 * Instead of returning whether the ICover is a TAUTOLOGY or not, it determines the cubes that causes the TAUTOLOGY.
 * <br>The method <code>compute(...)</code> returns a <code>List&lt;List&lt;ICube&gt;&gt;</code>, the List contains another List for each Leaf of the TAUTOLOGY-Algorithm containing all ICubes causing the TAUTOLOGY at this specific Leaf.
 *<br>Please Note that the ICubes are modified during the Algorithm and need to be marked externally to identify them later.
 * 
 * 
 * @author Jan
 *
 */
public class SimpleFindTautology {
	
	private enum SpecialCase {
		NONE, TAUTOLOGY, NO_TAUTOLOGY
	}
	
	
	private List<List<ICube>> result;
	private IGlobalInformation info;
	
	public SimpleFindTautology(IGlobalInformation info) {
		this.info = info;
	}
	
	public List<List<ICube>> compute(ICover cover) {
		
		long measurementId = Statistics.startMeasurement("FIND_TAUTOLOGY");
		
		result = new ArrayList<List<ICube>>();

		recursiveTautologyCheck(cover);
		
		Statistics.stopMeasurement(measurementId);
		
		return result;
			
		
					
	}
	
	private boolean recursiveTautologyCheck(ICover cover) {
		


		// Check Special Cases:
		
		SpecialCase sc = specialCase(cover);

		if (sc.equals(SpecialCase.NO_TAUTOLOGY))
			return false;
		else if (sc.equals(SpecialCase.TAUTOLOGY)) {
			return true;
		}
			

		// TODO: UNATE_REDUCTION, COMPONENT_REDUCTION

		
		
		//Binate Select:
		
		int literalPosition = cover.getMostBinateLiteral();
		
		ICube dcCube = CubeFactory.getDontCareCube(info);
		
		ICube splittingCubeLeft = dcCube.clone();
		splittingCubeLeft.setLiteral(literalPosition, ICube.DIRECT);
				
		ICube splittingCubeRight = dcCube;
		splittingCubeRight.setLiteral(literalPosition, ICube.NEGATED);		
		
		//Recursive call:
		

		if (!recursiveTautologyCheck(cover
				.getCofactor(splittingCubeLeft)))
			return false;
		
		

		if (!recursiveTautologyCheck(cover
				.getCofactor(splittingCubeRight)))
			return false;
		

		return true;

	}

	private SpecialCase specialCase(ICover cover) {

		/*
		 * Check for row of Don't Cares.
		 */
		
		boolean tautologyFound = false;
		List<ICube> resultEntry = new ArrayList<ICube>();
		
		for (ICube cube : cover) {
			if (cube.isTautology()) {
				tautologyFound = true;
				resultEntry.add(cube);				
			}
				
		}
		
		if(tautologyFound) {
			result.add(resultEntry);
			return SpecialCase.TAUTOLOGY;
		}
			
		
		if(cover.isUnate())
			return SpecialCase.NO_TAUTOLOGY;
		
		/*
		 * Equals the check, if there is a literal which only appears in one
		 * form: NEGATED or DIRECT form. (Book p. 65 Fig. 4.2.1 special case 2)
		 */
		assert(!cover.isEmpty()) : "Cover should not be empty at this point!";
		
		ICube andCube = cover.get(0).clone();
		ICube orCube = cover.get(0).clone();
		for (ICube cube : cover) {
			andCube = andCube.and(cube);
			orCube = orCube.or(cube);
		}

		int numberOfLiterals = cover.getNumberOfLiterals();

		for (int i = 0; i < numberOfLiterals; i++) {
			byte orLiteral = orCube.getLiteral(i);
			byte andLiteral = andCube.getLiteral(i);
			if (orLiteral==andLiteral&&orLiteral!=ICube.DONT_CARE)				
				return SpecialCase.NO_TAUTOLOGY;
		}

		/*
		 * (Book p. 65 Fig. 4.2.1 special case 3)
		 */
		if ((cover.getUpperBoundOfMinterms()) < (2 ^ numberOfLiterals))
			return SpecialCase.NO_TAUTOLOGY;

		// if(numberOfLiterals<8) {
		// //TODO: truth table , minterm test.
		// }

		return SpecialCase.NONE;
	}
}
